MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { append(@l1, @l2) -> append#1(@l1, @l2) , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) , append#1(nil(), @l2) -> @l2 , subtrees(@t) -> subtrees#1(@t) , subtrees#1(leaf()) -> nil() , subtrees#1(node(@x, @t1, @t2)) -> subtrees#2(subtrees(@t1), @t1, @t2, @x) , subtrees#2(@l1, @t1, @t2, @x) -> subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x) , subtrees#3(@l2, @l1, @t1, @t2, @x) -> ::(node(@x, @t1, @t2), append(@l1, @l2)) } Obligation: innermost runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Fastest' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'matrix interpretation of dimension 4' failed due to the following reason: The input cannot be shown compatible 2) 'matrix interpretation of dimension 3' failed due to the following reason: The input cannot be shown compatible 3) 'matrix interpretation of dimension 3' failed due to the following reason: The input cannot be shown compatible 4) 'matrix interpretation of dimension 2' failed due to the following reason: The input cannot be shown compatible 5) 'matrix interpretation of dimension 2' failed due to the following reason: The input cannot be shown compatible 6) 'matrix interpretation of dimension 1' failed due to the following reason: The input cannot be shown compatible 2) 'Fastest' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'custom shape polynomial interpretation' failed due to the following reason: The input cannot be shown compatible 2) 'linear polynomial interpretation' failed due to the following reason: The input cannot be shown compatible 3) 'custom shape polynomial interpretation' failed due to the following reason: The input cannot be shown compatible Arrrr..